es:ES, e:E, P:({a:E| loc(a) = loc(e)  Id} ).
(a:{a:E| loc(a) = loc(e)  Id} . Dec(P(a)))
 (e'e.P(e')
  (e':E. (e' loc e  c (P(e') & (e'':E. (e' <loc e'')  e'' loc e   (P(e''))))))) 

latex

Definitions	True, T, ee'.P(e), {T}, SQType(T), x. t(x), (e <loc e'), P & Q, e loc e' , A c B, x:A. B(x), P  Q, e@i. P(e), t  T, x(s), P  Q, , x:A. B(x), A, False, P  Q, P  Q, Dec(P)
Lemmas	es-locl transitivity1, es-pred-locl, es-le-pred, true wf, squash wf, es-locl irreflexivity, es-le weakening, es-locl transitivity2, es-le wf, es-le weakening eq, es-locl-iff, es-loc-pred, alle-le wf, es-first wf, assert wf, not wf, es-causl wf, es-le-loc, Id sq, es-locl wf, alle-at-iff, event system wf, decidable wf, es-loc wf, Id wf, es-E wf